Nuprl Lemma : es-le-pred 0,22

the_es:ES, ee':E. first(e' (e  pred(e')   (e <loc e')) 
latex


Definitionst  T, P  Q, x:AB(x), pred(e), E, Prop, (e <loc e'), P  Q, {T}, e  e' , first(e), b, A, P & Q, P  Q, P  Q, ES
Lemmasevent system wf, iff functionality wrt iff, es-locl-iff, es-le wf, not wf, assert wf, es-first wf, es-locl wf, es-E wf, es-pred wf

origin